import type {Type} from './type.js'
import {type FreeVariableTerm, type VariableTerm, QuantifiedVariableTerm} from './term.js'
import {Formula} from './formula.js'
import * as Rules from './inferences.js'
import {map, pipe, reduce, reverse} from './iterator.js'

const inferences: readonly ((premises: Formula[], consequence: Formula) => boolean)[] = [
    Rules.insertTrue,
    Rules.insertOr,
    Rules.insertAnd,
    Rules.insertEx,
    Rules.insertIs,
    Rules.insertEquality,
    Rules.eliminateFalse,
    Rules.eliminateOr,
    Rules.eliminateImplies,
    Rules.eliminateAnd,
    Rules.eliminateFor,
    Rules.reiterate,
]

const lastFormulaIndex = -1

export class Verifier {
    types: Record<string, Type | undefined>
    formulae: Record<number, Formula | undefined>
    variables: Record<string, VariableTerm | undefined>
    reservations: Record<string, Type | undefined>
    referencedFormulae: Formula[] = []

    static readonly defaultType = {name: '_unknown_', baseTypes: []}
    static readonly defaultVariable = new QuantifiedVariableTerm({
        name: '_unknown_',
        type: this.defaultType,
    })

    constructor(parentVerifier?: Verifier) {
        this.types = Object.create(parentVerifier?.types || null) as Verifier['types']
        this.formulae = Object.create(parentVerifier?.formulae || null) as Verifier['formulae']
        this.variables = Object.create(parentVerifier?.variables || null) as Verifier['variables']
        this.reservations = Object.create(parentVerifier?.reservations || null) as Verifier['reservations']
        this.clearLastFormula()
    }

    addType(name: string, baseTypes: Type[]) {
        if (this.types[name])
            return false

        this.types[name] = {name, baseTypes}

        return true
    }

    reserve(name: string, type: Type) {
        this.reservations[name] = type
    }

    getReservedType(name: string) {
        return this.reservations[name]
    }

    addBoundVariable(variable: QuantifiedVariableTerm) {
        this.variables = Object.create(this.variables) as Verifier['variables']
        return this._addVariable(variable)
    }

    addFreeVariable(variable: FreeVariableTerm) {
        return this._addVariable(variable)
    }

    private _addVariable<T extends VariableTerm>(variable: T): T {
        this.variables[variable.name] = variable
        return variable
    }

    removeBoundVariable() {
        this.variables = Object.getPrototypeOf(this.variables) as Verifier['variables']
    }

    resolveVariable(name: string) {
        return this.variables[name]
    }

    addFormula(label: number, formula: Formula) {
        this.formulae[label] = formula
        this.formulae[lastFormulaIndex] = formula
    }

    referenceLastFormula() {
        const formula = this.formulae[lastFormulaIndex]
        this.referencedFormulae.push(formula || Formula.True)
        this.formulae[lastFormulaIndex] = undefined

        return !!formula
    }

    clearLastFormula() {
        this.formulae[lastFormulaIndex] = undefined
    }

    referenceFormulaByLabel(label: number) {
        const referencedFormula = this.formulae[label]

        if (!referencedFormula)
            return false

        this.referencedFormulae.push(referencedFormula)
        return true
    }

    verify(formula: Formula, premises = this.referencedFormulae) {
        if (premises === this.referencedFormulae)
            this.referencedFormulae = []

        return inferences.some(infer => infer(premises, formula))
    }

    verifyConsider(variables: FreeVariableTerm[], clauses: Formula[], premises = this.referencedFormulae) {
        if (premises === this.referencedFormulae)
            this.referencedFormulae = []

        const baseFormula = pipe(
            clauses.length ? clauses : [Formula.True],
            reverse,
            reduce((formula, clause) => new Formula.Conjunction([clause, formula])),
        )

        if (baseFormula === Formula.True)
            return true

        const variableMap = pipe(
            variables,
            map(variable => [
                variable,
                new QuantifiedVariableTerm(variable),
            ] as const),
            entries => new Map(entries),
        )

        const formula = pipe(
            variables,
            reverse,
            reduce(
                (formula, variable) => new Formula.Existence(variable, formula),
                baseFormula,
            ),
            formula => formula.substitute(variableMap),
        )

        return Rules.reiterate(premises, formula)
    }
}
